The class forcing theorem, which asserts that every class forcing notion ${\mathbb {P}}$ admits a forcing relation $\Vdash _{\mathbb {P}}$, that is, a relation satisfying the forcing relation recursion—it follows that statements true in the corresponding forcing extensions are forced and forced statements are true—is equivalent over Gödel–Bernays set theory $\text {GBC}$ to the principle of elementary transfinite recursion $\text {ETR}_{\text {Ord}}$ for class recursions of length $\text {Ord}$. It is also equivalent to the existence of truth predicates for the (...) infinitary languages $\mathcal {L}_{\text {Ord},\omega }$, allowing any class parameter A; to the existence of truth predicates for the language $\mathcal {L}_{\text {Ord},\text {Ord}}$ ; to the existence of $\text {Ord}$ -iterated truth predicates for first-order set theory $\mathcal {L}_{\omega,\omega }$ ; to the assertion that every separative class partial order ${\mathbb {P}}$ has a set-complete class Boolean completion; to a class-join separation principle; and to the principle of determinacy for clopen class games of rank at most $\text {Ord}+1$. Unlike set forcing, if every class forcing notion ${\mathbb {P}}$ has a forcing relation merely for atomic formulas, then every such ${\mathbb {P}}$ has a uniform forcing relation applicable simultaneously to all formulas. Our results situate the class forcing theorem in the rich hierarchy of theories between $\text {GBC}$ and Kelley–Morse set theory $\text {KM}$. (shrink)

We introduce the $\Sigma _1$ -definable universal finite sequence and prove that it exhibits the universal extension property amongst the countable models of set theory under end-extension. That is, the sequence is $\Sigma _1$ -definable and provably finite; the sequence is empty in transitive models; and if M is a countable model of set theory in which the sequence is s and t is any finite extension of s in this model, then there is an end-extension of M to a (...) model in which the sequence is t. Our proof method grows out of a new infinitary-logic-free proof of the Barwise extension theorem, by which any countable model of set theory is end-extended to a model of $V=L$ or indeed any theory true in a suitable submodel of the original model. The main theorem settles the modal logic of end-extensional potentialism, showing that the potentialist validities of the models of set theory under end-extensions are exactly the assertions of S4. Finally, we introduce the end-extensional maximality principle, which asserts that every possibly necessary sentence is already true, and show that every countable model extends to a model satisfying it. (shrink)

We explain and explore class-theoretic potentialism—the view that one can always individuate more classes over a set-theoretic universe. We examine some motivations for class-theoretic potentialism, before proving some results concerning the relevant potentialist systems (in particular exhibiting failures of the $\mathsf {.2}$ and $\mathsf {.3}$ axioms). We then discuss the significance of these results for the different kinds of class-theoretic potentialists.

Given a countable model of set theory, we study the structure of its generic multiverse, the collection of its forcing extensions and ground models, ordered by inclusion. Mostowski showed that any finite poset embeds into the generic multiverse while preserving the nonexistence of upper bounds. We obtain several improvements of his result, using what we call the blockchain construction to build generic objects with varying degrees of mutual genericity. The method accommodates certain infinite posets, and we can realize these embeddings (...) via a wide variety of forcing notions, while providing control over lower bounds as well. We also give a generalization to class forcing in the context of second-order set theory, and exhibit some further structure in the generic multiverse, such as the existence of exact pairs. (shrink)

In this article I investigate the phenomenon of minimum and minimal models of second-order set theories, focusing on Kelley–Morse set theory KM, Gödel–Bernays set theory GB, and GB augmented with the principle of Elementary Transfinite Recursion. The main results are the following. (1) A countable model of ZFC has a minimum GBC-realization if and only if it admits a parametrically definable global well order. (2) Countable models of GBC admit minimal extensions with the same sets. (3) There is no minimum (...) transitive model of KM. (4) There is a minimum β-model of GB+ETR. The main question left unanswered by this article is whether there is a minimum transitive model of GB+ETR. (shrink)

We present a class forcing notion, uniformly definable for ordinals η, which forces the ground model to be the ηth inner mantle of the extension, in which the sequence of inner mantles has length at least η. This answers a conjecture of Fuchs, Hamkins, and Reitz [1] in the positive. We also show that forces the ground model to be the ηth iterated of the extension, where the sequence of iterated s has length at least η. We conclude by showing (...) that the lengths of the sequences of inner mantles and of iterated s can be separated to be any two ordinals you please. (shrink)

A theory T is tight if different deductively closed extensions of T (in the same language) cannot be bi-interpretable. Many well-studied foundational theories are tight, including $\mathsf {PA}$ [39], $\mathsf {ZF}$, $\mathsf {Z}_2$, and $\mathsf {KM}$ [6]. In this article we extend Enayat’s investigations to subsystems of these latter two theories. We prove that restricting the Comprehension schema of $\mathsf {Z}_2$ and $\mathsf {KM}$ gives non-tight theories. Specifically, we show that $\mathsf {GB}$ and $\mathsf {ACA}_0$ each admit different bi-interpretable extensions, (...) and the same holds for their extensions by adding $\Sigma ^1_k$ -Comprehension, for $k \ge 1$. These results provide evidence that tightness characterizes $\mathsf {Z}_2$ and $\mathsf {KM}$ in a minimal way. (shrink)